////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009 The Mist project                                        //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the implementation of the prove function.
///

#include "findproof.hpp"

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include <stack>
using std::stack;

#include <boost/assign.hpp>
using namespace boost::assign;

#include <boost/foreach.hpp>
#define foreach BOOST_FOREACH
#define foreach_reverse BOOST_REVERSE_FOREACH

#include "common/assert.hpp"
#include "common/ptr.hpp"
#include "copyast.hpp"
#include "findreferences.hpp"
#include "nodes.hpp"
#include "parse.hpp"
#include "symbol.hpp"
#include "tree.hpp"
#include "navigator.hpp"

				#include <iostream>
				using std::cerr;

////////////////////////////////////////////////////////////////////////////////
// ProofPhase Type                                                            //
////////////////////////////////////////////////////////////////////////////////

enum ProofTotality {
	PARTIAL_CORRECTNESS,
	  TOTAL_CORRECTNESS
};

////////////////////////////////////////////////////////////////////////////////
// Function Predeclarations                                                   //
////////////////////////////////////////////////////////////////////////////////

bool can_try_correctness_proof(wptr<FunctionDeclaration> function, ProofTotality phase);
void     try_correctness_proof(wptr<FunctionDeclaration> function, ProofTotality phase);

////////////////////////////////////////////////////////////////////////////////
// find_proof Function                                                        //
////////////////////////////////////////////////////////////////////////////////

class FindProofVisitor : public Navigator {
	public:
		
		VISIT_FUNCTIONS_FROM( (FunctionDeclaration) )
		
		ProofTotality phase;
};

////////////////////////////////////////////////////////////////////////////////

void find_proof(wptr<Node> ast) {
	assert(ast);
	
	sptr<FindProofVisitor> visitor(new FindProofVisitor);
	
	visitor->phase = TOTAL_CORRECTNESS;
	ast->accept(visitor);
	
	visitor->phase = PARTIAL_CORRECTNESS;
	ast->accept(visitor);
}

////////////////////////////////////////////////////////////////////////////////

void FindProofVisitor::visit(wptr<FunctionDeclaration> function) {
	assert(function);
	
	if (can_try_correctness_proof(function, phase))
		try_correctness_proof(function, phase);
	
	Navigator::visit(function);
}

////////////////////////////////////////////////////////////////////////////////
// can_try_correctness_proof Function                                         //
////////////////////////////////////////////////////////////////////////////////

class CanTryProofVisitor : public Navigator {
	public:
		
		VISIT_FUNCTIONS_FROM (
			(FunctionDeclaration)
			(WhileStatement)
			(FunctionCall)
		)
		
		bool canTry;
		bool totalKeyProofsInsufficient;
		wptr<Symbol> functionUnderInvestigation;
		ProofTotality phase;
};

////////////////////////////////////////////////////////////////////////////////

bool can_try_correctness_proof(wptr<FunctionDeclaration> function, ProofTotality phase) {
	sptr<CanTryProofVisitor> visitor(new CanTryProofVisitor);
	visitor->canTry = true;
	visitor->totalKeyProofsInsufficient = false;
	visitor->functionUnderInvestigation = function->paramScope();
	visitor->phase = phase;
	
	(*function->body.begin())->accept(visitor);
	
	visitor->canTry &= (function->post.size() > 0);
	
	if (phase == PARTIAL_CORRECTNESS) {
		visitor->totalKeyProofsInsufficient |= (!function->totalPreImplicationSolver || function->totalPreImplicationSolver->proof_status() != KeySolver::PROVED);
		visitor->canTry &= visitor->totalKeyProofsInsufficient;
	}
	
	return visitor->canTry;
}

////////////////////////////////////////////////////////////////////////////////

void CanTryProofVisitor::visit(wptr<FunctionDeclaration> node) {
	assert(node);
}

void CanTryProofVisitor::visit(wptr<WhileStatement> node) {
	assert(node);
	
	canTry &= (node->invariant.size() > 0);
	
	if (phase == TOTAL_CORRECTNESS) {
		canTry &= (node->bound.size() > 0);
	} else {
		totalKeyProofsInsufficient |= (!node-> totalPreImplicationSolver || node-> totalPreImplicationSolver->proof_status() != KeySolver::PROVED);
		totalKeyProofsInsufficient |= (!node->totalPostImplicationSolver || node->totalPostImplicationSolver->proof_status() != KeySolver::PROVED);
	}
	
	if (!canTry)
		return;
	
	Navigator::visit(node);
}

void CanTryProofVisitor::visit(wptr<FunctionCall> node) {
	assert(node);
	
	if (phase == TOTAL_CORRECTNESS) {
		assert(typeid(*node->base) == typeid(Reference));
		canTry &= (node->base.cast<Reference>()->symbol() != functionUnderInvestigation
		       ||  functionUnderInvestigation->declaration->bound.size() > 0);
	}
	
	if (!canTry)
		return;
	
	Navigator::visit(node);
}

////////////////////////////////////////////////////////////////////////////////
// try_correctness_proof Function                                             //
////////////////////////////////////////////////////////////////////////////////

class BuildProofOutlineVisitor : public Navigator {
	public:
		
		VISIT_FUNCTIONS_FROM (
			(AssertionArea)
			(CompoundStatement)
			(FunctionDeclaration)
			(FunctionCall)
			(IfStatement)
			(OperatorCall)
			(VariableDeclaration)
			(WhileStatement)
		)
		
		ProofTotality phase;
};

sptr<Expression> copy_with_absolute_paths(wptr<Expression> expr, wptr<Symbol> scope);

////////////////////////////////////////////////////////////////////////////////

void try_correctness_proof(wptr<FunctionDeclaration> function, ProofTotality phase) {
	assert(function);
	
	sptr<BuildProofOutlineVisitor> visitor(new BuildProofOutlineVisitor);
	
	visitor->phase = phase;
	
	// Pre
	//
	sptr<Expression> pre;
	if (function->pre.size()) {
		foreach (wptr<AssertionArea> aa, function->pre) {
			foreach (wptr<Expression> cond, aa->conditions) {
				if (!pre) {
					pre = cond;
				} else {
					sptr<Expression> old = pre;
					pre = parse<Expression>("%1 and %2", function->paramScope(), list_of( old )( cond ));
				}
			}
		}
	} else {
		pre = parse<Expression>("true", function->paramScope());
	}
	
	// Post
	//
	sptr<Expression> post;
	if (function->post.size()) {
		foreach (wptr<AssertionArea> aa, function->post) {
			foreach (wptr<Expression> cond, aa->conditions) {
				if (!post) {
					post = cond;
				} else {
					sptr<Expression> old = post;
					post = parse<Expression>("%1 and %2", function->resultScope(), list_of( old )( cond ));
				}
			}
		}
	} else {
		post = parse<Expression>("true", function->resultScope());
	}
	
	// Set the postcondition of the function body.
	//
	if (phase == TOTAL_CORRECTNESS)
		(*function->body.begin())->totalPostcondition = copy(post, (*function->body.begin())->introducedScope());
	else
		(*function->body.begin())->partialPostcondition = copy(post, (*function->body.begin())->introducedScope());
	
	// Find the weakest precondition of the function body.
	//
	(*function->body.begin())->accept(visitor);
	
	if (phase == TOTAL_CORRECTNESS) {
		// Register the implication to be proved.
		//
		if (function->bound.size()) {
			function->totalPreImplicationSolver = n_sptr(new KeySolver(
				parse<Expression>("%1 and 0 <= %2 = oldbound ==> %3", Symbol::construct_scope((*function->body.begin())->scope()), list_of
					( copy(pre)                                          ) // 1
					( copy(*function->bound.begin())                     ) // 2
					( copy((*function->body.begin())->totalPrecondition) ) // 3
				)
			));
		} else {
			function->totalPreImplicationSolver = n_sptr(new KeySolver(
				parse<Expression>("%1 ==> %2", Symbol::construct_scope((*function->body.begin())->scope()), list_of
					( copy(pre)                                          ) // 1
					( copy((*function->body.begin())->totalPrecondition) ) // 2
				)
			));
		}
		function->totalPreImplicationSolver->start_key();
	} else {
		// Register the implication to be proved.
		//
		function->partialPreImplicationSolver = n_sptr(new KeySolver(
			parse<Expression>("%1 ==> %2", Symbol::construct_scope((*function->body.begin())->scope()), list_of
				( copy(pre)                                            ) // 1
				( copy((*function->body.begin())->partialPrecondition) ) // 2
			)
		));
		function->partialPreImplicationSolver->start_key();
	}
}

////////////////////////////////////////////////////////////////////////////////

void BuildProofOutlineVisitor::visit(wptr<AssertionArea> node) {
	assert(node);
	
	if (phase == TOTAL_CORRECTNESS) {
		sptr<Expression> condition = copy(node->totalPostcondition);
		foreach (wptr<Expression> cond, node->conditions)
			condition = parse<Expression>("%1 and %2", Symbol::construct_scope(node->scope()), list_of( condition )( copy(cond) ));
		node->totalPrecondition = condition;
	} else {
		sptr<Expression> condition = copy(node->partialPostcondition);
		foreach (wptr<Expression> cond, node->conditions)
			condition = parse<Expression>("%1 and %2", Symbol::construct_scope(node->scope()), list_of( condition )( copy(cond) ));
		node->partialPrecondition = condition;
	}
}

void BuildProofOutlineVisitor::visit(wptr<CompoundStatement> node) {
	assert(node);
	
	if (phase == TOTAL_CORRECTNESS) {
		if (node->statements.size() == 0) {
			node->totalPrecondition = node->totalPostcondition;
		} else {
			node->totalPostcondition = copy_with_absolute_paths(node->totalPostcondition, Symbol::construct_scope(node->introducedScope()));
			node->statements.back()->totalPostcondition = node->totalPostcondition;
			
			for (int i = node->statements.size() - 1; i >= 0; --i) {
				node->statements[i]->accept(wptr_this());
				if (i != 0)
					node->statements[i-1]->totalPostcondition = node->statements[i]->totalPrecondition;
			}
			
			node->totalPrecondition = node->statements.front()->totalPrecondition;
		}
	} else {
		if (node->statements.size() == 0) {
			node->partialPrecondition = node->partialPostcondition;
		} else {
			node->partialPostcondition = copy_with_absolute_paths(node->partialPostcondition, Symbol::construct_scope(node->introducedScope()));
			node->statements.back()->partialPostcondition = node->partialPostcondition;
			
			for (int i = node->statements.size() - 1; i >= 0; --i) {
				node->statements[i]->accept(wptr_this());
				if (i != 0)
					node->statements[i-1]->partialPostcondition = node->statements[i]->partialPrecondition;
			}
			
			node->partialPrecondition = node->statements.front()->partialPrecondition;
		}
	}
}

void BuildProofOutlineVisitor::visit(wptr<FunctionDeclaration> node) {
	assert(node);
	
	if (phase == TOTAL_CORRECTNESS)
		node->totalPrecondition = node->totalPostcondition;
	else
		node->partialPrecondition = node->partialPostcondition;
}

void BuildProofOutlineVisitor::visit(wptr<FunctionCall> node) {
	assert(node);
	
	assert(typeid(*node->base) == typeid(Reference));
	
	wptr<Symbol> function = node->base.cast<Reference>()->symbol();
	
	assert(function->declaration);
	
	// Find the precondition of the function
	//
	sptr<Expression> functionPre;
	if (function->declaration->pre.size()) {
		foreach (wptr<AssertionArea> aa, function->declaration->pre) {
			foreach (wptr<Expression> cond, aa->conditions) {
				if (!functionPre) {
					functionPre = cond;
				} else {
					sptr<Expression> old = functionPre;
					functionPre = parse<Expression>("%1 and %2", function->declaration->paramScope(), list_of( old )( cond ));
				}
			}
		}
	} else {
		functionPre = parse<Expression>("true", node->scope());
	}
	
	// Find the postcondition of the function
	//
	sptr<Expression> functionPost;
	if (function->declaration->post.size()) {
		foreach (wptr<AssertionArea> aa, function->declaration->post) {
			foreach (wptr<Expression> cond, aa->conditions) {
				if (!functionPost) {
					functionPost = cond;
				} else {
					sptr<Expression> old = functionPost;
					functionPost = parse<Expression>("%1 and %2", function->declaration->resultScope(), list_of( old )( cond ));
				}
			}
		}
	} else {
		functionPost = parse<Expression>("true", node->scope());
	}
	
	wptr<FunctionDeclaration> callingFunction;
	{
		wptr<Node> current = node;
		while (typeid(*current) != typeid(FunctionDeclaration))
			current = current->parent;
		callingFunction = current.cast<FunctionDeclaration>();
	}
	
	// Fetch the simple-form logical vars from the called function precondition
	//
	map<wptr<Symbol>, sptr<Node> > logicalVarSimpleForms = logical_var_simple_forms(function->declaration);
	
	if (phase == TOTAL_CORRECTNESS) {
		// Find the references to program variables in the postcondition of this
		// call and the postcondition of the called function.
		//
		set<wptr<Symbol> > references;
		foreach (wptr<Symbol> ref, find_references(node->totalPostcondition))
			if (ref->access == AccessType(true, true, false))
				references.insert(ref);
		foreach (wptr<Symbol> ref, find_references(functionPost))
			if (ref->access == AccessType(true, true, false))
				references.insert(ref);
		
		map<wptr<Symbol>, string> varToLogicalName;
		foreach (wptr<Symbol> var, references)
			varToLogicalName[var] = new_unique_identifier(node->scope()->root, *var->name);
		
		typedef std::pair<wptr<Symbol>, string> Pair;
		foreach (Pair p, varToLogicalName) {
			sptr<Declaration> newDecl = parse<Declaration>((string)echo(p.first->type) + " " + p.second + ";", callingFunction->paramScope());
			newDecl->parent = callingFunction;
			callingFunction->logicalVars.insert(newDecl.cast<VariableDeclaration>());
		}
		
		// Create the varToLogicalReference map.
		//
		map<wptr<Symbol>, sptr<Node> > varToLogicalReference;
		std::pair<wptr<Symbol>, string> p;
		foreach (p, varToLogicalName)
			varToLogicalReference[p.first] = parse<Reference>(p.second, node->scope());
		
		// Calculate total precondition of function-call
		//
		if (function->declaration == callingFunction) {
			// Recursion
			
			node->totalPrecondition = parse<Expression>("%1 and 0 <= %2 < oldbound and (%3 ==> %4)", Symbol::construct_scope(node->scope()), list_of
				( copy(functionPre, logicalVarSimpleForms, node->scope())                                              ) // 1
				( copy(*function->declaration->bound.begin(), map<wptr<Symbol>, sptr<Node> >(), node->scope())         ) // 2
				( copy(copy(functionPost, varToLogicalReference, node->scope()), logicalVarSimpleForms, node->scope()) ) // 3
				( copy(node->totalPostcondition, varToLogicalReference, node->scope())                                 ) // 4
			);
		} else {
			// No Recursion
			
			// Calculate total precondition of function-call
			//
			node->totalPrecondition = parse<Expression>("%1 and (%2 ==> %3)", Symbol::construct_scope(node->scope()), list_of
				( copy(functionPre, logicalVarSimpleForms, node->scope())                               ) // 1
				( copy(copy(functionPost, varToLogicalReference), logicalVarSimpleForms, node->scope()) ) // 2
				( copy(node->totalPostcondition, varToLogicalReference, node->scope())                  ) // 3
			);
		}
	} else {
		// Find the references to program variables in the postcondition of this
		// call and the postcondition of the called function.
		//
		set<wptr<Symbol> > references;
		foreach (wptr<Symbol> ref, find_references(node->partialPostcondition))
			if (ref->access == AccessType(true, true, false) && !is_function_local(ref, node->scope()))
				references.insert(ref);
		foreach (wptr<Symbol> ref, find_references(functionPost))
			if (ref->access == AccessType(true, true, false))
				references.insert(ref);
		
		map<wptr<Symbol>, string> varToLogicalName;
		foreach (wptr<Symbol> var, references)
			varToLogicalName[var] = new_unique_identifier(node->scope()->root, *var->name);
		
		typedef std::pair<wptr<Symbol>, string> Pair;
		foreach (Pair p, varToLogicalName) {
			sptr<Declaration> newDecl = parse<Declaration>((string)echo(p.first->type) + " " + p.second + ";", callingFunction->paramScope());
			newDecl->parent = callingFunction;
			callingFunction->logicalVars.insert(newDecl.cast<VariableDeclaration>());
		}
		
		// Create the varToLogicalReference map.
		//
		map<wptr<Symbol>, sptr<Node> > varToLogicalReference;
		std::pair<wptr<Symbol>, string> p;
		foreach (p, varToLogicalName)
			varToLogicalReference[p.first] = parse<Reference>(p.second, node->scope());
		
		// Calculate partial precondition of function-call
		//
		node->partialPrecondition = parse<Expression>("(%1 ==> %2) ==> %3", Symbol::construct_scope(node->scope()), list_of
			( copy(functionPre, logicalVarSimpleForms, node->scope())                                              ) // 1
			( copy(copy(functionPost, logicalVarSimpleForms, node->scope()), varToLogicalReference, node->scope()) ) // 2
			( copy(node->partialPostcondition, varToLogicalReference, node->scope())                               ) // 3
		);
	}
}

void BuildProofOutlineVisitor::visit(wptr<IfStatement> node) {
	assert(node);
	
	// Set thenStatement postcondition
	//
	if (phase == TOTAL_CORRECTNESS)
		node->thenStatement->totalPostcondition = node->totalPostcondition;
	else
		node->thenStatement->partialPostcondition = node->partialPostcondition;
	
	// Find thenStatement weakest precondition
	//
	node->thenStatement->accept(wptr_this());
	
	// ElsePart
	//
	if (node->elseStatement) {
		// Set elseStatement postcondition
		//
		if (phase == TOTAL_CORRECTNESS)
			node->elseStatement->totalPostcondition = node->totalPostcondition;
		else
			node->elseStatement->partialPostcondition = node->partialPostcondition;
		
		// Find elseStatement weakest precondition
		//
		node->elseStatement->accept(wptr_this());
	}
	
	sptr<Expression> partialImpliedByNotCond, totalImpliedByNotCond;
	if (node->elseStatement) {
		partialImpliedByNotCond = node->elseStatement->partialPrecondition;
		  totalImpliedByNotCond = node->elseStatement->  totalPrecondition;
	} else {
		partialImpliedByNotCond = node->partialPostcondition;
		  totalImpliedByNotCond = node->  totalPostcondition;
	}
	
	if (phase == TOTAL_CORRECTNESS)
		node->totalPrecondition = parse<Expression>("(%1 ==> %2) and (!%3 ==> %4)", Symbol::construct_scope(node->scope()), list_of
			( copy(node->condition)                        ) // 1
			( copy(node->thenStatement->totalPrecondition) ) // 2
			( copy(node->condition)                        ) // 3
			( copy(totalImpliedByNotCond)                  ) // 4
		);
	else
		node->partialPrecondition = parse<Expression>("(%1 ==> %2) and (!%3 ==> %4)", Symbol::construct_scope(node->scope()), list_of
			( copy(node->condition)                          ) // 1
			( copy(node->thenStatement->partialPrecondition) ) // 2
			( copy(node->condition)                          ) // 3
			( copy(partialImpliedByNotCond)                  ) // 4
		);
}

void BuildProofOutlineVisitor::visit(wptr<OperatorCall> node) {
	assert(node);
	
	assert(typeid(*node->op) == typeid(SingleOperator));
	
	if (node->op.cast<SingleOperator>()->function_name() == "assign") {
		if (typeid(*node->operands[0]) == typeid(Reference)) {
			map<wptr<Symbol>, sptr<Node> > mp;
			
			mp[node->operands[0].cast<Reference>()->symbol()] = copy(node->operands[1], Symbol::construct_scope(node->scope())); // Maybe not good?
			
			if (phase == TOTAL_CORRECTNESS)
				node->totalPrecondition = copy(node->totalPostcondition, mp, Symbol::construct_scope(node->scope()));
			else
				node->partialPrecondition = copy(node->partialPostcondition, mp, Symbol::construct_scope(node->scope()));
		} else if (typeid(*node->operands[0]) == typeid(OperatorCall) &&
		           *node->operands[0].cast<OperatorCall>()->op == SingleOperator("1 [ 2 ]") &&
		           typeid(*node->operands[0].cast<OperatorCall>()->operands[0]) == typeid(Reference)) {
			
			if (phase == TOTAL_CORRECTNESS)
				node->totalPrecondition = copy(node->totalPostcondition,
				                               node->operands[0].cast<OperatorCall>()->operands[0].cast<Reference>()->symbol(),
				                               node->operands[0].cast<OperatorCall>()->operands[1],
				                               copy(node->operands[1], Symbol::construct_scope(node->scope())),
				                               Symbol::construct_scope(node->scope()));
			else
				node->partialPrecondition = copy(node->partialPostcondition,
				                                 node->operands[0].cast<OperatorCall>()->operands[0].cast<Reference>()->symbol(),
				                                 node->operands[0].cast<OperatorCall>()->operands[1],
				                                 copy(node->operands[1], Symbol::construct_scope(node->scope())),
				                                 Symbol::construct_scope(node->scope()));
		} else {
			if (phase == TOTAL_CORRECTNESS)
				node->totalPrecondition = node->totalPostcondition;
			else
				node->partialPrecondition = node->partialPostcondition;
		}
	} else {
		if (phase == TOTAL_CORRECTNESS)
			node->totalPrecondition = node->totalPostcondition;
		else
			node->partialPrecondition = node->partialPostcondition;
	}
}

void BuildProofOutlineVisitor::visit(wptr<VariableDeclaration> node) {
	assert(node);
	
	sptr<Expression> partialCondition, totalCondition;
	if (phase == TOTAL_CORRECTNESS)
		totalCondition = node->totalPostcondition;
	else
		partialCondition = node->partialPostcondition;
	
	foreach_reverse (VariableDeclaration::Pair pair, node->pairs) {
		if (pair.init) {
			map<wptr<Symbol>, sptr<Node> > mp;
			
			mp[parse<Reference>(pair.name->text, node->scope())->symbol()] = copy(pair.init, Symbol::construct_scope(node->scope()));
			
			if (phase == TOTAL_CORRECTNESS)
				totalCondition = copy(totalCondition, mp, Symbol::construct_scope(node->scope()));
			else
				partialCondition = copy(partialCondition, mp, Symbol::construct_scope(node->scope()));
		}
	}
	
	if (phase == TOTAL_CORRECTNESS)
		node->totalPrecondition = totalCondition;
	else
		node->partialPrecondition = partialCondition;
}

void BuildProofOutlineVisitor::visit(wptr<WhileStatement> node) {
	assert(node);
	
	// Invariant
	//
	sptr<Expression> invariant;
	if (node->invariant.size()) {
		foreach (wptr<AssertionArea> aa, node->invariant) {
			foreach (wptr<Expression> cond, aa->conditions) {
				if (!invariant) {
					invariant = cond;
				} else {
					sptr<Expression> old = invariant;
					invariant = parse<Expression>("%1 and %2", Symbol::construct_scope(node->scope()), list_of( old )( cond ));
				}
			}
		}
	} else {
		invariant = parse<Expression>("true", node->scope());
	}
	
	if (phase == TOTAL_CORRECTNESS) {
		// Implication to be proved: !cond and invar ==> totalPostcondition
		//
		node->totalPostImplicationSolver = n_sptr(new KeySolver(
			parse<Expression>("!%1 and %2 ==> %3", Symbol::construct_scope(node->scope()), list_of
				( copy(node->condition)          ) // 1
				( copy(invariant)                ) // 2
				( copy(node->totalPostcondition) ) // 3
			)
		));
		
		node->totalPostImplicationSolver->start_key();
	} else {
		// Implication to be proved: !cond and invar ==> partialPostcondition
		//
		node->partialPostImplicationSolver = n_sptr(new KeySolver(
			parse<Expression>("!%1 and %2 ==> %3", Symbol::construct_scope(node->scope()), list_of
				( copy(node->condition)            ) // 1
				( copy(invariant)                  ) // 2
				( copy(node->partialPostcondition) ) // 3
			)
		));
		
		node->partialPostImplicationSolver->start_key();
	}
	
	// Set the postcondition of the statement
	//
	if (phase == TOTAL_CORRECTNESS) {
		(*node->statement.begin())->totalPostcondition = parse<Expression>("%1 and 0 <= %2 < oldbound", Symbol::construct_scope((*node->statement.begin())->introducedScope()), list_of
			( copy(invariant)            ) // 1
			( copy(*node->bound.begin()) ) // 2
		);
	} else {
		(*node->statement.begin())->partialPostcondition = copy(invariant);
	}
	
	// Find the weakest precondition of the statement.
	//
	(*node->statement.begin())->accept(wptr_this());
	
	
	if (phase == TOTAL_CORRECTNESS) {
		// Implication to be proved: cond and invar and 0 < bound = oldbound ==> statement.weakest_totalPrecondition
		//
		node->totalPreImplicationSolver = n_sptr(new KeySolver(
			parse<Expression>("%1 and %2 and 0 < %3 = oldbound ==> %4", Symbol::construct_scope((*node->statement.begin())->introducedScope()), list_of
				( copy(node->condition)                    ) // 1
				( copy(invariant)                          ) // 2
				( copy(*node->bound.begin())               ) // 3
				( copy((*node->statement.begin())->totalPrecondition) ) // 4
			)
		));
		
		// Start KeY on the proof.
		//
		node->totalPreImplicationSolver->start_key();
	} else {
		// Implication to be proved: cond and invar ==> statement.weakest_partialPrecondition
		//
		node->partialPreImplicationSolver = n_sptr(new KeySolver(
			parse<Expression>("%1 and %2 ==> %3", Symbol::construct_scope((*node->statement.begin())->introducedScope()), list_of
				( copy(node->condition)                      ) // 1
				( copy(invariant)                            ) // 2
				( copy((*node->statement.begin())->partialPrecondition) ) // 3
			)
		));
		
		// Start KeY on the proof.
		//
		node->partialPreImplicationSolver->start_key();
	}
	
	// While loop precondition = invariant
	//
	if (phase == TOTAL_CORRECTNESS) {
		node->totalPrecondition = parse<Expression>("%1 and 0 <= %2", Symbol::construct_scope((*node->statement.begin())->scope()), list_of
			( copy(invariant)            ) // 1
			( copy(*node->bound.begin()) ) // 2
		);
	} else {
		node->partialPrecondition = copy(invariant);
	}
}

////////////////////////////////////////////////////////////////////////////////

sptr<Expression> copy_with_absolute_paths(wptr<Expression> expr, wptr<Symbol> scope) {
	set<wptr<Symbol> > references = find_references(expr);
	
	map<wptr<Symbol>, sptr<Node> > mp;
	foreach (wptr<Symbol> ref, references)
		mp[ref] = ref->create_absolute_reference(scope);
	
	sptr<Expression> result = copy(expr, mp, scope);
	
	return result;
}
